$\forall$$T$:Type, $r$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$), $S$:Type, $f$:($S$$\rightarrow$$T$). \\[0ex]WellFnd\{i\}($T$;$x$,$y$.$r$($x$,$y$)) $\Rightarrow$ WellFnd\{i\}($S$;$x$,$y$.$r$($f$($x$),$f$($y$)))